perm filename CATSET.GEN[EKL,SYS] blob
sn#825882 filedate 1988-08-04 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00015 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 (wipe-out)
C00004 00003 (proof setfunct)
C00006 00004 (proof cat)
C00008 00005 (proof catfacts)
C00011 00006 (proof facts)
C00014 00007 (proof ontoepic)
C00017 00008 (proof injmonic)
C00020 00009 (proof right_inverse)
C00022 00010 (proof inverse)
C00025 00011 (proof ontomap_composition)
C00027 00012 (proof bijections_composition)
C00030 00013 (proof bijections_identity_inverse)
C00035 00014 (proof injmap_composition)
C00039 00015 bug-catching
C00042 ENDMK
C⊗;
(wipe-out)
(proof set)
(decl (xv yv zv) (type: ground) (sort: urelement))
(decl (set a b c d) (type: |ground→truthval|))
(decl (f g h) (type: |ground→ground|))
(decl epsilon (type: |ground⊗@a→truthval|) (infixname: ε) (bindingpower: 925))
(define epsilon |∀a xv.xvεa≡a(xv)|)
(label epsilondef)
(axiom |∀a b.(∀xv.xvεa≡xvεb)⊃a=b|)
(label set_extensionality)
(decl intersection (type: |@a⊗@a→@a|)
(infixname: ∩) (bindingpower: 950) (prefixname: intersection))
(define intersection |∀a b.a∩b=λxv.(a(xv)∧b(xv))|)
(label interdef)
(decl union (type: |@a⊗@a→@a|)
(infixname: ∪) (bindingpower: 950) (prefixname: union))
(define union |∀a b.a∪b=λxv.(a(xv)∨b(xv))|)
(label uniondef)
(decl inclusion (type: |@a⊗@a→truthval|)
(infixname: ⊂) (bindingpower: 920) (prefixname: inclusion))
(define inclusion |∀a b.a⊂b≡∀xv.a(xv)⊃b(xv)|)
(label inclusiondef)
(defax emptyset |emptyset=λxv.false|)
(defax emptyp |∀a.emptyp(a)=∀xv.¬a(xv)|)
;the set of occurrences of an element
(decl mkset (type: |ground→@a|))
(define mkset |∀xv.mkset(xv)=(λyv.yv=xv)|)
(label mkset_def)
(axiom |∀a b.a⊂b∧b⊂a⊃a=b|)
(label double_inclusion)
(proof setfunct)
(decl map (type: |@f⊗@a⊗@a→truthval|))
(define map |∀g a b.map(g,a,b)≡(∀xv.xvεa⊃g(xv)εb)|)
(label mapdef)
(decl invim (type: |@f⊗ground→@a|))
(define invim |∀g a yv.invim(g,yv)= λxv.g(xv)=yv|)
(label invimdef)
(decl ontomap (type: |@f⊗@a⊗@a→truthval|))
(define ontomap |∀g a b.ontomap(g,a,b)≡map(g,a,b)∧(∀zv.zvεb⊃(∃yv.yvεa∧g(yv)=zv))|)
(label ontomapdef)
(decl injmap (type: |@f⊗@a⊗@a→truthval|))
(define injmap |∀g a b.injmap(g,a,b)≡map(g,a,b)∧(∀xv yv.xvεa ∧ yvεa ∧ g(xv)=g(yv) ⊃ xv=yv)|)
(label injmapdef)
(decl bijection (type: |@f⊗@a⊗@a→truthval|))
(define bijection |∀g a b.bijection(g,a,b)≡ontomap(g,a,b)∧injmap(g,a,b)|)
(label bijectiondef)
(proof cat)
(decl compmap (type: |@g⊗@g→@g|)(infixname: ⊗⊗) (bindingpower: 960))
(define compmap |∀f g.f⊗⊗g=(λxv.f(g(xv)))|)
(label compmapdef)
(define f_id |f_id=λyv.yv|)
(label fid_def)
(decl id (type: |@a→@f|))
(define id |∀a xv.xvεa⊃(id(a))(xv)=f_id(xv)|)
(label id)
(decl isomorphism (type: |@g⊗@a⊗@a→truthval|))
(define isomorphism
|∀g a b. isomorphism(g,a,b)≡
(map(g,a,b)∧(∃h.map(h,b,a)∧h ⊗⊗ g=id(a)∧g ⊗⊗ h=id(b)))|)
(label isomorphism)
(axiom |∀f g a b.map(f,a,b)∧map(g,a,b) ∧ (∀xv.xvεa⊃f(xv)=g(xv)) ⊃ f=g|)
(label function_extensionality)
(decl epic (type: |@g⊗@a⊗@a→truthval|))
(define epic |∀f a b.epic(f,a,b)≡map(f,a,b)∧
(∀g h c.map(g,b,c)∧map(h,b,c)∧g⊗⊗f=h⊗⊗f⊃g=h)|)
(label epicdef)
(decl monic (type: |@g⊗@a⊗@a→truthval|))
(define monic |∀f b c.monic(f,b,c)≡map(f,b,c)∧
(∀g h a.map(g,a,b)∧map(h,a,b)∧f⊗⊗g=f⊗⊗h⊃g=h)|)
(label monicdef)
(proof catfacts)
(axiom |∀f xv.urelement f(xv)|)
(label simpinfo)
(axiom |∀f g a b c.map(f,a,b) ∧ map(g,b,c) ⊃ map(g⊗⊗f,a,c)|)
(label compmap)
(axiom |∀a.map(id(a),a,a)|)
(label idmap)
(axiom |∀f g h a b c d.map(f,a,b)∧map(g,b,c)∧map(h,c,d)⊃
(h⊗⊗g)⊗⊗f=h⊗⊗(g⊗⊗f)|)
(label function_associativity)
(axiom |∀f g a b c.ontomap(f,a,b)∧ontomap(g,b,c)⊃ontomap(g ⊗⊗ f,a,c)|)
(label ontomap_composition)
(axiom |∀f g a b c.injmap(g ⊗⊗ f,a,c)∧map(f,a,b)⊃injmap(f,a,b)|)
(label injmap_composition1)
(axiom |∀f g a b c.injmap(g ⊗⊗ f,a,c)∧ontomap(f,a,b)∧map(g,b,c)⊃injmap(g,b,c)|)
(label injmap_composition2)
(axiom |∀f a b.map(f,a,b)⊃id(b)⊗⊗f=f|)
(label identity_left)
(axiom |∀f a b.map(f,a,b)⊃f⊗⊗id(a)=f|)
(label identity_right)
(axiom |∀f a b.ontomap(f,a,b)⊃epic(f,a,b)|)
(label ontoepic)
(axiom |∀f a b.injmap(f,a,b)⊃monic(f,a,b)|)
(label injmonic)
(axiom |∀g a b.bijection(g,a,b)⊃(∃f.map(f,b,a)∧g⊗⊗f=id(b))|)
(label right_inverse)
(axiom |∀g a b.bijection(g,a,b)⊃(∃f.map(f,b,a)∧f⊗⊗g=id(a)∧g⊗⊗f=id(b))|)
(label twosided_inverse)
;main facts:
;BIJECTION(F,A,B)∧BIJECTION(G,B,C)⊃BIJECTION(G⊗⊗F,A,C)
(axiom |∀f g a b c.bijection(f,a,b)∧bijection(g,b,c)⊃bijection(g⊗⊗f,a,c)|)
(label bijection_composition)
;BIJECTION(ID(A),A,A)
(axiom |∀a.bijection(id(a),a,a)|)
(label bijection_identity)
;BIJECTION(G,A,B)⊃(∃F.BIJECTION(F,B,A)∧F⊗⊗G=ID(A)∧G⊗⊗F=ID(B))
(axiom |∀g a b.bijection(g,a,b)⊃(∃f.bijection(f,b,a)∧f⊗⊗g=id(a)∧g⊗⊗f=id(b))|)
(label bijection_inverse)
(save-proofs catset)
(proof facts)
;theorem 1
;compmap
1. (trw |∀f g a b c.map(f,a,b) ∧ map(g,b,c) ⊃ map(g⊗⊗f,a,c)|
(open map compmap epsilon))
;∀F G A B C.MAP(F,A,B)∧MAP(G,B,C)⊃MAP(G ⊗⊗ F,A,C)
;function_associativity
2. (trw |∀f g h a b c d xv.map(f,a,b) ∧ map(g,b,c) ∧ map(h,c,d)⊃
map((h⊗⊗g)⊗⊗f,a,d) ∧ map(h⊗⊗(g⊗⊗f),a,d) ∧
(xvεa⊃((h⊗⊗g)⊗⊗f)(xv)=(h⊗⊗(g⊗⊗f))(xv))|
(open map compmap epsilon) )
;∀F G H A B C D X.MAP(F,A,B)∧MAP(G,B,C)∧MAP(H,C,D)⊃
; MAP((H ⊗⊗ G) ⊗⊗ F,A,D)∧MAP(H ⊗⊗ (G ⊗⊗ F),A,D)∧
; (XεA⊃((H ⊗⊗ G) ⊗⊗ F)(X)=(H ⊗⊗ (G ⊗⊗ F))(X))
; (derive |∀f g h a b c d.map(f,a,b)∧map(g,b,c)∧map(h,c,d)⊃
; (h⊗⊗g)⊗⊗f=h⊗⊗(g⊗⊗f)| (* function_extensionality))
3. (assume |map(f,a,b)∧map(g,b,c)∧map(h,c,d)|)
4. (ue ((f.|(h ⊗⊗ g) ⊗⊗ f|)(g.|h ⊗⊗ (g ⊗⊗ f)|)(a.a)(b.d))
function_extensionality * -2)
;(H ⊗⊗ G) ⊗⊗ F=H ⊗⊗ (G ⊗⊗ F)
5. (ci -2)
;MAP(F,A,B)∧MAP(G,B,C)∧MAP(H,C,D)⊃(H ⊗⊗ G) ⊗⊗ F=H ⊗⊗ (G ⊗⊗ F)
;theorem 2
;idmap
6. (trw |map(id(set),set,set)| (open map id f_id))
;MAP(ID(SET),SET,SET)
;identity left
7. (trw |∀f a b xv.map(f,a,b)∧xvεa⊃(id(b)⊗⊗f)(xv)=f(xv)|
(open map compmap id f_id))
;∀F A B X.MAP(F,A,B)∧XεA⊃(ID(B)⊗⊗F)(X)=F(X)
8. (ue ((f.|id(b)⊗⊗f|)(g.|f|)(a.a)(b.b)) function_extensionality
compmap idmap *)
;MAP(F,A,B)⊃ID(B)⊗⊗F=F
;identity_right
9. (trw |∀f a b xv.map(f,a,b)∧xvεa⊃(f⊗⊗id(a))(xv)=f(xv)|
(open map compmap id f_id))
;∀F A B X.MAP(F,A,B)∧XεA⊃(F⊗⊗ID(A))(X)=F(X)
10. (ue ((f.|f⊗⊗id(a)|)(g.|f|)(a.a)(b.b)) function_extensionality
compmap idmap *)
;MAP(F,A,B)⊃F⊗⊗ID(A)=F
(proof ontoepic)
1. (assume |ontomap(f,a,b)|)
(label oe1)
2. (assume |map(g,b,c)∧map(h,b,c)|)
(label oe2)
3. (assume |g⊗⊗f=h⊗⊗f|)
(label oe3)
4. (assume |g≠h|)
(label oe4)
5. (ue ((f.g)(g.h)(a.b)(b.c)) function_extensionality
oe2 oe4)
;¬(∀X.XεB⊃G(X)=H(X))
;deps: (OE2 OE4)
6. (define yvv |¬(yvvεb⊃g(yvv)=h(yvv))| *)
;YVV is unknown.
;the symbol YYV is given the same declaration as YV
;deps: (OE2 OE4)
7. (derive |yvvεb∧g(yvv)≠h(yvv)| *)
(label oe5)
;deps: (OE2 OE4)
8. (rw oe1 (open ontomap))
;MAP(F,A,B)∧(∀Z.ZεB⊃(∃Y.YεA∧F(Y)=Z))
(label oe6)
;deps: (OE1)
9. (define xvv |xvvεa ∧ f(xvv)=yvv| (oe5 oe6))
(label oe7)
;xvv is unknown.
;the symbol xvv is given the same declaration as xv
;deps: (OE1 OE2 OE4)
10. (trw |(g⊗⊗f)(xvv)| (use oe3 mode: exact))
;(G⊗⊗F)(XXV)=(H⊗⊗F)(XXV)
;deps: (OE3)
11. (rw * (open compmap) (use oe7 mode: always) oe5)
;FALSE
;deps: (OE1 OE2 OE3 OE4)
12. (ci oe4)
;G=H
;deps: (OE1 OE2 OE3)
13. (ci (oe2 oe3))
;MAP(G,B,C)∧MAP(H,B,C)∧G⊗⊗F=H⊗⊗F⊃G=H
;deps: (OE1)
14. (trw |epic(f,a,b)| (open epic) oe6 *)
;EPIC(F,A,B)
;deps: (OE1)
15. (ci oe1)
;ONTOMAP(F,A,B)⊃EPIC(F,A,B)
(proof injmonic)
1. (assume |injmap(f,b,c)|)
(label im1)
2. (assume |map(g,a,b)∧map(h,a,b)|)
(label im2)
;deps: (2)
3. (assume |f⊗⊗g=f⊗⊗h|)
(label im3)
4. (assume |g≠h|)
(label im4)
5. (ue ((f.g)(g.h)(a.a)(b.b)) function_extensionality
im2 im4)
;¬(∀X.XεA⊃G(X)=H(X))
;deps: (IM2 IM4)
6. (define xww |¬(xwwεa⊃g(xww)=h(xww))| *)
;XWW is unknown.
;the symbol XWW is given the same declaration as XV
;deps: (IM2 IM4)
7. (derive |xwwεa∧g(xww)≠h(xww)| *)
(label im5)
;deps: (IM2 IM4)
8. (trw |(f⊗⊗g)(xww)| (use im3 mode: exact))
;(F⊗⊗G)(XWW)=(F⊗⊗H)(XWW)
(label im6)
;deps: (IM3)
9. (rw * (open compmap))
;F(G(XWW))=F(H(XWW))
;deps: (IM3)
(label im7)
10. (rw im2 (open map))
;(∀X.XεA⊃G(X)εB)∧(∀X.XεA⊃H(X)εB)
;deps: (IM2)
11. (derive |g(xww)εb ∧ h(xww)εb| (* im5))
(label im8)
;deps: (IM2 IM4)
12. (rw im1 (open injmap))
;MAP(F,B,C)∧(∀X Y.XεB∧YεB∧F(X)=F(Y)⊃X=Y)
(label im9)
;deps: (IM1)
13. (ue ((xv.|g(xww)|)(yv.|h(xww)|)) * (im7 im8 im5))
;FALSE
;deps: (IM1 IM2 IM3 IM4)
14. (ci im4)
;G=H
;deps: (IM1 IM2 IM3)
15. (ci (im2 im3))
;MAP(G,A,B)∧MAP(H,A,B)∧F⊗⊗G=F⊗⊗H⊃G=H
;deps: (IM1)
16. (trw |monic(f,b,c)| (open monic) * im9)
;MONIC(F,B,C)
;deps: (IM1)
17. (ci im1)
;INJMAP(F,B,C)⊃MONIC(F,B,C)
(proof right_inverse)
1. (assume |bijection(g,a,b)|)
(label inv1)
2. (rw * (open bijection ontomap))
;MAP(G,A,B)∧(∀Z.ZεB⊃(∃Y.YεA∧G(Y)=Z))∧INJMAP(G,A,B)
(label inv2)
;deps: (INV1)
3. (derive |∀zv.∃yv.zvεb⊃yvεa∧g(yv)=zv| *)
;deps: (INV1)
;right inverse:
4. (define fv |∀zv.zvεb⊃fv(zv)εa∧g(fv(zv))=zv| *)
(label inv3)
;FV is unknown.
;the symbol FV is given the same declaration as F
;deps: (INV1)
5. (trw |map(fv,b,a) ∧ (∀zv.zvεb⊃g(fv(zv))=f_id(zv))|(open map f_id) *)
;MAP(FV,B,A)∧(∀Z.ZεB⊃G(FV(Z))=F_ID(Z))
(label inv4)
;deps: (INV1)
6. (trw |map(fv,b,a) ∧ ∀zv.zvεb⊃(g⊗⊗fv)(zv)=(id(b))(zv)|
(open compmap) (use id) *)
;MAP(FV,B,A)∧(∀Z.ZεB⊃(G⊗⊗FV)(Z)=(ID(B))(Z))
(label inv5)
;deps: (INV1)
7. (derive |map(g⊗⊗fv,b,b)| (compmap inv2 inv5))
(label inv6)
;deps: (INV1)
8. (ue ((f.|g⊗⊗fv|)(g.|id(b)|)(a.b)(b.b)) function_extensionality
idmap inv5 inv6)
;G⊗⊗FV=ID(B)
(label inv7)
;deps: (INV1)
9. (derive |∃f.map(f,b,a)∧g⊗⊗f=id(b)| (inv5 inv7))
;deps: (INV1)
10. (ci inv1)
;BIJECTION(G,A,B)⊃(∃F.MAP(F,B,A)∧G⊗⊗F=ID(B))
(proof inverse)
1. (assume |bijection(g,a,b)|)
(label inv10)
2. (rw * (open bijection ontomap))
;MAP(G,A,B)∧(∀Z.ZεB⊃(∃Y.YεA∧G(Y)=Z))∧INJMAP(G,A,B)
(label inv11)
;deps: (INV10)
3. (define fv |map(fv,b,a) ∧ g⊗⊗fv=id(b)| (right_inverse inv10))
(label inv12)
;FV is unknown.
;the symbol FV is given the same declaration as F
;deps: (INV10)
4. (derive |map(fv⊗⊗g,a,a)| (compmap inv11 inv12))
(label inv13)
;deps: (INV10)
5. (trw |(g⊗⊗fv)⊗⊗g=id(b)⊗⊗g| inv12)
;(G⊗⊗FV)⊗⊗G=ID(B)⊗⊗G
;deps: (INV10)
6. (rw * (use function_associativity
ue: ((f.g)(g.|fv|)(h.g)(a.a)(b.b)(c.a)(d.b)) mode: exact)
inv11 inv12 idmap
(use identity_left ue: ((f.g)(a.a)(b.b)) mode: exact))
;G⊗⊗(FV⊗⊗G)=G
;deps: (INV10)
7. (trw |g⊗⊗(fv⊗⊗g)=g⊗⊗id(a)| *
(use identity_right ue: ((f.g)(a.a)(b.b)) mode: exact)
inv11)
;G⊗⊗(FV⊗⊗G)=G⊗⊗ID(A)≡G=G
;deps: (INV10)
8. (rw *)
;G⊗⊗(FV⊗⊗G)=G⊗⊗ID(A)
(label inv14)
;deps: (INV10)
9. (derive |monic(g,a,b)| (injmonic inv11))
;deps: (INV10)
10. (rw * (open monic) inv11)
;∀G1 H A1.MAP(G1,A1,A)∧MAP(H,A1,A)∧G⊗⊗G1=G⊗⊗H⊃G1=H
;deps: (INV10)
11. (ue ((g1.|fv⊗⊗g|)(h.|id(a)|)(a1.a)(a.a)) * inv13 idmap inv14)
;FV⊗⊗G=ID(A)
;deps: (INV10)
12. (derive |∃f.map(f,b,a)∧f⊗⊗g=id(a)∧g⊗⊗f=id(b)| (* inv12))
;deps: (INV10)
13. (ci inv10)
;BIJECTION(G,A,B)⊃(∃F.MAP(F,B,A)∧F⊗⊗G=ID(A)∧G⊗⊗F=ID(B))
(proof ontomap_composition)
1. (assume |ontomap(f,a,b)∧ontomap(g,b,c)|)
(label oc1)
2. (rw * (open ontomap epsilon))
;MAP(F,A,B)∧(∀Z.B(Z)⊃(∃Y.A(Y)∧F(Y)=Z))∧
;MAP(G,B,C)∧(∀Z.C(Z)⊃(∃Y.B(Y)∧G(Y)=Z))
(label oc2)
;deps: (OC1)
3. (assume |c(zv)|)
(label oc3)
4. (define yw |b(yw) ∧ g(yw)=zv| (oc2 oc3))
(label oc4)
;YW is unknown.
;the symbol YW is given the same declaration as YV
;deps: (OC1 OC3)
5. (define xw |a(xw) ∧ f(xw)=yw| (oc2 oc4))
;XW is unknown.
;the symbol XW is given the same declaration as XV
;deps: (OC1 OC3)
6. (trw |a(xw) ∧ g(f(xw))=zv| (use * mode: always) oc4)
;A(XW)∧G(F(XW))=Z
;deps: (OC1 OC3)
7. (derive |∃yv.a(yv) ∧ g(f(yv))=zv| *)
;deps: (OC1 OC3)
8. (ci oc3)
;C(Z)⊃(∃Y.A(Y)∧G(F(Y))=Z)
;deps: (OC1)
9. (trw |ontomap(g ⊗⊗ f,a,c)| (open ontomap compmap epsilon)
(* oc2 compmap))
;ONTOMAP(G ⊗⊗ F,A,C)
;deps: (OC1)
10. (ci oc1)
;ONTOMAP(F,A,B)∧ONTOMAP(G,B,C)⊃ONTOMAP(G ⊗⊗ F,A,C)
(proof bijections_composition)
1. (assume |bijection(f,a,b)∧bijection(g,b,c)|)
(label bic1)
;deps: (1)
2. (rw * (open bijection injmap epsilon))
;ONTOMAP(F,A,B)∧MAP(F,A,B)∧(∀X Y.A(X)∧A(Y)∧F(X)=F(Y)⊃X=Y)∧
;ONTOMAP(G,B,C)∧MAP(G,B,C)∧(∀X Y.B(X)∧B(Y)∧G(X)=G(Y)⊃X=Y)
(label bic2)
;deps: (BIC1)
3. (derive |ontomap(g ⊗⊗ f,a,c)| (* ontomap_composition))
(label bic3)
;deps: (BIC1)
4. (assume |a(x1) ∧ a(x2)|)
(label bic6)
5. (assume |g(f(x1))=g(f(x2))|)
(label bic7)
6. (trw |map(f,a,b)| bic2)
;MAP(F,A,B)
;deps: (BIC1)
7. (rw * (open map epsilon))
;∀X.A(X)⊃B(F(X))
;deps: (BIC1)
8. (derive |b(f(x1)) ∧ b(f(x2))| (* bic6))
;deps: (BIC1 BIC6)
9. (derive |f(x1)=f(x2)| (bic2 bic7 *))
;deps: (BIC1 BIC6 BIC7)
10. (derive |x1=x2| (bic2 bic6 *))
;deps: (BIC1 BIC6 BIC7)
11. (ci (bic6 bic7))
;A(X1)∧A(X2)∧G(F(X1))=G(F(X2))⊃X1=X2
;deps: (BIC1)
12. (trw |injmap(g ⊗⊗ f,a,c)| (open injmap epsilon compmap)
(* bic2 compmap))
;INJMAP(G ⊗⊗ F,A,C)
(label bic8)
;deps: (BIC1)
13. (trw |bijection(g⊗⊗f,a,c)| (open bijection) (bic3 bic8))
;BIJECTION(G ⊗⊗ F,A,C)
;deps: (BIC1)
14. (ci bic1)
;BIJECTION(F,A,B)∧BIJECTION(G,B,C)⊃BIJECTION(G⊗⊗F,A,C)
(proof bijections_identity_inverse)
1. (trw |bijection(id(a),a,a)| (open bijection ontomap injmap id f_id) idmap)
;BIJECTION(ID(A),A,A)
2. (assume |bijection(g,a,b)|)
(label bii1)
3. (define fv |map(fv,b,a)∧fv⊗⊗g=id(a)∧g⊗⊗fv=id(b)| (twosided_inverse bii1))
(label bii2)
;deps: (BII1)
4. (assume |xvεa|)
(label bii3)
5. (trw |(fv⊗⊗g)(xv)=xv| (use bii2 mode: always) (open id f_id) bii3)
;(FV⊗⊗G)(X)=X
;deps: (BII1 BII3)
6. (rw * (open compmap))
;FV(G(X))=X
(label bii4)
;deps: (BII1 BII3)
7. (rw bii1 (open bijection ontomap map))
;(∀X.XεA⊃G(X)εB)∧(∀Z.ZεB⊃(∃Y.YεA∧G(Y)=Z))∧INJMAP(G,A,B)
(label bii5)
;deps: (BII1)
8. (derive |g(xv)εb∧fv(g(xv))=xv| (bii3 bii4 bii5))
;deps: (BII1 BII3)
9. (ci bii3)
;XεA⊃G(X)εB∧FV(G(X))=X
;deps: (BII1)
10. (derive |ontomap(fv,b,a)| (bii2 *) (open ontomap))
(label bii6)
;deps: (BII1)
11. (assume |x1εb ∧ x2εb ∧ fv(x1)=fv(x2)|)
(label bii10)
12. (trw |g(fv(x1))| (use * mode: always))
;G(FV(X1))=G(FV(X2))
(label bii11)
;deps: (BII10)
13. (trw |(g⊗⊗fv)(x1)| (open compmap))
;(G⊗⊗FV)(X1)=G(FV(X1))
14. (trw |(g⊗⊗fv)(x2)| (open compmap))
;(G⊗⊗FV)(X2)=G(FV(X2))
15. (trw |(g⊗⊗fv)(x1)=(g⊗⊗fv)(x2)| (use * -2 mode: exact))
;(G⊗⊗FV)(X1)=(G⊗⊗FV)(X2)≡G(FV(X1))=G(FV(X2))
16. (derive |(g⊗⊗fv)(x1)=(g⊗⊗fv)(x2)| (* bii11))
;deps: (BII10)
17. (rw * (use bii2 mode: exact) (open id f_id) bii10)
;X1=X2
;deps: (BII1 BII10)
18. (ci bii10)
;X1εB∧X2εB∧FV(X1)=FV(X2)⊃X1=X2
;deps: (BII1)
19. (trw |injmap(fv,b,a)| (open injmap) bii2 *)
;INJMAP(FV,B,A)
(label bii12)
;deps: (BII1)
20. (trw |bijection(fv,b,a)| (open bijection) bii6 bii12)
;BIJECTION(FV,B,A)
;deps: (BII1)
21. (derive |∃f.bijection(f,b,a)∧f⊗⊗g=id(a)∧g⊗⊗f=id(b)| (* bii2))
;deps: (BII1)
22. (ci bii1)
;BIJECTION(G,A,B)⊃(∃F.BIJECTION(F,B,A)∧F⊗⊗G=ID(A)∧G⊗⊗F=ID(B))
(proof injmap_composition)
1. (assume |injmap(g ⊗⊗ f,a, c)|)
(label ic1)
2. (assume |map(f,a,b)|)
(label ic2)
3. (rw ic1 (open injmap compmap epsilon))
;MAP(λX.G(F(X)),A,C)∧(∀X Y.A(X)∧A(Y)∧G(F(X))=G(F(Y))⊃X=Y)
(label ic4)
;deps: (IC1)
4. (assume |a(xv)∧a(yv)∧f(xv)=f(yv)|)
(label ic5)
5. (derive |xv=yv| (ic4 *))
;deps: (IC1 IC5)
6. (ci ic5)
;A(X)∧A(Y)∧F(X)=F(Y)⊃X=Y
;deps: (IC1)
7. (trw |injmap(f,a,b)| (open injmap epsilon) ic2 *)
;INJMAP(F,A,B)
;deps: (IC1 IC2)
8. (ci (ic1 ic2))
;INJMAP(G ⊗⊗ F,A,C)∧MAP(F,A,B)⊃INJMAP(F,A,B)
;second part:
9. (assume |ontomap(f,a,b)|)
(label ic10)
10. (assume |map(g,b,c)|)
(label ic11)
11. (assume |b(xv)∧b(yv)∧g(xv)=g(yv)|)
(label ic12)
12. (rw ic10 (open ontomap epsilon))
;MAP(F,A,B)∧(∀Z.B(Z)⊃(∃Y.A(Y)∧F(Y)=Z))
(label ic13)
;deps: (IC10)
13. (define xz |a(xz)∧f(xz)=xv| (ic12 ic13))
;XZ is unknown.
(label ic14)
;the symbol XZ is given the same declaration as XV
;deps: (IC10 IC12)
14. (define yz |a(yz)∧f(yz)=yv| (ic12 ic13))
(label ic15)
;YZ is unknown.
;the symbol YZ is given the same declaration as YV
;deps: (IC10 IC12)
15. (trw |(g ⊗⊗ f)(xz)=(g ⊗⊗ f)(yz)| (open compmap)
(use ic14 ic15 mode: always) ic12)
;(G ⊗⊗ F)(XZ)=(G ⊗⊗ F)(YZ)
(label ic16)
;deps: (IC10 IC12)
16. (rw ic1 (open injmap epsilon))
;MAP(G ⊗⊗ F,A,C)∧(∀X Y.A(X)∧A(Y)∧(G ⊗⊗ F)(X)=(G ⊗⊗ F)(Y)⊃X=Y)
;deps: (IC1)
17. (trw |∀xv yv.a(xv)∧a(yv)∧(g ⊗⊗ f)(xv)=(g ⊗⊗ f)(yv)⊃xv=yv| *)
;∀X Y.A(X)∧A(Y)∧(G ⊗⊗ F)(X)=(G ⊗⊗ F)(Y)⊃X=Y
;deps: (IC1)
18. (ue ((xv.|xz|)(yv.|yz|)) * (ic14 ic15 ic16))
;XZ=YZ
;deps: (IC1 IC10 IC12)
19. (trw |xv=yv| (use ic14 ic15 * mode: always direction: reverse))
;X=Y
;deps: (IC1 IC10 IC12)
20. (ci ic12)
;B(X)∧B(Y)∧G(X)=G(Y)⊃X=Y
;deps: (IC1 IC10)
21. (trw |injmap(g,b,c)| (open injmap epsilon) * ic11)
;INJMAP(G,B,C)
;deps: (IC1 IC10 IC11)
22. (ci (ic1 ic10 ic11))
;INJMAP(G ⊗⊗ F,A,C)∧ONTOMAP(F,A,B)∧MAP(G,B,C)⊃INJMAP(G,B,C)
;bug-catching
(wipe-out)
(proof foo)
(setq rewritemessages t)
(decl (x y z) (type: ground))
(decl (f g h) (type: |ground→ground|))
(decl compmap (type: |@g⊗@g→@g|)(infixname: ⊗⊗) (bindingpower: 960))
(define compmap |∀f g.f⊗⊗g=(λx.f(g(x)))|)
(label compmapdef)
(assume |G(F(X1))=G(F(X2))|)
(trw |(g⊗⊗f)(x1)=(g⊗⊗f)(x2)| (open compmap) *)